/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRK30



␈↓ ↓H␈↓α␈↓ ∧→A DIFFICULT VERIFICATION PROBLEM

␈↓ ↓H␈↓␈↓ α_Consider␈α⊂a␈α⊃graph␈α⊂defined␈α⊂by␈α⊃a␈α⊂function␈α⊃␈↓↓successors␈↓.␈α⊂ We␈α⊂are␈α⊃interested␈α⊂in␈α⊃defining␈α⊂and
␈↓ ↓H␈↓proving␈α
correct␈α
a␈α
LISP␈α∞function␈α
for␈α
computing␈α
the␈α
component␈α∞␈↓↓component␈α
x␈↓␈α
of␈α
a␈α
vertex␈α∞␈↓↓x␈↓.␈α
 The
␈↓ ↓H␈↓component can be defined by the formula

␈↓ ↓H␈↓␈↓ α_␈↓↓∀␈α∂x␈α∂y:[y␈α∞ε␈α∂component␈α∂x␈α∞≡␈α∂∃␈α∂u:␈α∞x␈α∂=␈α∂␈↓αa␈↓↓␈α∞u␈α∂∧␈α∂y␈α∞=␈α∂last␈α∂u␈α∞∧␈α∂∀␈α∂z1␈α∞z2:[precedes[z1,z2,u]␈α∂⊃␈α∂z2␈α∞ε
␈↓ ↓H␈↓↓successors z1]]␈↓,

␈↓ ↓H␈↓where ␈↓↓precedes[z1,z2,u]␈↓ is recursively defined by

␈↓ ↓H␈↓␈↓ α_␈↓↓precedes[z1,z2,u] = ¬␈↓αn␈↓↓ u ∧ [[z1 = ␈↓αa␈↓↓ u ∧ ¬␈↓αn␈↓↓ ␈↓αd␈↓↓ u ∧ z2 = ␈↓αad␈↓↓ u] ∨ precedes[z1,z2,␈↓αd␈↓↓ u]]␈↓.

␈↓ ↓H␈↓␈↓ α_Our␈αobject␈α
is␈αto␈α
define␈αa␈αLISP␈α
function␈αcomputing␈α
␈↓↓component␈αx␈↓␈αand␈α
to␈αprove␈α
that␈αit␈α
is␈αin
␈↓ ↓H␈↓accordance␈αwith␈αthe␈αabove␈αpredicate␈αcalculus␈αdefinition.␈α In␈αorder␈αthat␈αthis␈αshould␈αbe␈αpossible␈αwe
␈↓ ↓H␈↓need␈αan␈αaxiom␈αstating␈αthat␈αthe␈αfunction␈α␈↓↓successors␈↓␈αleads␈αonly␈αto␈αa␈αfinite␈αgraph.␈α This␈αcan␈αbe␈αdone
␈↓ ↓H␈↓in␈αseveral␈αways,␈αand␈α
one␈αof␈αthe␈αsimplest␈α
is␈αto␈αassert␈αthe␈α
existence␈αof␈αan␈αinteger␈α
␈↓↓N␈↓␈αthat␈αis␈αan␈α
upper
␈↓ ↓H␈↓bound on the length of a successor chain.

␈↓ ↓H␈↓␈↓ α_A candidate function is

␈↓ ↓H␈↓␈↓ α_␈↓↓component[x] = comp1[<x>,␈↓NIL␈↓↓]␈↓,

␈↓ ↓H␈↓where

␈↓ ↓H␈↓␈↓ α_␈↓↓comp[u,seen]␈α_=␈α_␈↓αif␈↓↓␈α_␈↓αn␈↓↓␈α_u␈α_␈↓αthen␈↓↓␈α_seen␈α_␈↓αelse␈↓↓␈α_␈↓αif␈↓↓␈α_␈↓αa␈↓↓␈α_u␈α_ε␈α_seen␈α_␈↓αthen␈↓↓␈α_comp[␈↓αd␈↓↓␈α_u,seen]␈α_␈↓αelse␈↓↓
␈↓ ↓H␈↓↓comp[successors[␈↓αa␈↓↓ u]*[␈↓αd␈↓↓ u],[␈↓αa␈↓↓ u].seen]␈↓.

␈↓ ↓H␈↓The␈α∩inductions␈α∩required␈α∩to␈α∪prove␈α∩that␈α∩this␈α∩or␈α∪any␈α∩other␈α∩solution␈α∩satisfies␈α∪the␈α∩specifications
␈↓ ↓H␈↓promise to be interesting.